* Step 1: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            activate(X) -> X
            activate(n__add(X1,X2)) -> add(X1,X2)
            activate(n__from(X)) -> from(X)
            activate(n__fst(X1,X2)) -> fst(X1,X2)
            activate(n__len(X)) -> len(X)
            add(X1,X2) -> n__add(X1,X2)
            add(0(),X) -> X
            add(s(X),Y) -> s(n__add(activate(X),Y))
            from(X) -> cons(X,n__from(s(X)))
            from(X) -> n__from(X)
            fst(X1,X2) -> n__fst(X1,X2)
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
            len(X) -> n__len(X)
            len(cons(X,Z)) -> s(n__len(activate(Z)))
            len(nil()) -> 0()
        - Signature:
            {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons
            ,n__add,n__from,n__fst,n__len,nil,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(n__add) = {1},
            uargs(n__fst) = {1,2},
            uargs(n__len) = {1},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [1]                    
            p(activate) = [10] x1 + [0]          
                 p(add) = [10] x1 + [10] x2 + [4]
                p(cons) = [1] x2 + [0]           
                p(from) = [0]                    
                 p(fst) = [10] x1 + [10] x2 + [0]
                 p(len) = [10] x1 + [0]          
              p(n__add) = [1] x1 + [1] x2 + [0]  
             p(n__from) = [0]                    
              p(n__fst) = [1] x1 + [1] x2 + [1]  
              p(n__len) = [1] x1 + [0]           
                 p(nil) = [0]                    
                   p(s) = [1] x1 + [1]           
          
          Following rules are strictly oriented:
          activate(n__fst(X1,X2)) = [10] X1 + [10] X2 + [10]               
                                  > [10] X1 + [10] X2 + [0]                
                                  = fst(X1,X2)                             
          
                       add(X1,X2) = [10] X1 + [10] X2 + [4]                
                                  > [1] X1 + [1] X2 + [0]                  
                                  = n__add(X1,X2)                          
          
                       add(0(),X) = [10] X + [14]                          
                                  > [1] X + [0]                            
                                  = X                                      
          
                      add(s(X),Y) = [10] X + [10] Y + [14]                 
                                  > [10] X + [1] Y + [1]                   
                                  = s(n__add(activate(X),Y))               
          
                       fst(0(),Z) = [10] Z + [10]                          
                                  > [0]                                    
                                  = nil()                                  
          
              fst(s(X),cons(Y,Z)) = [10] X + [10] Z + [10]                 
                                  > [10] X + [10] Z + [1]                  
                                  = cons(Y,n__fst(activate(X),activate(Z)))
          
          
          Following rules are (at-least) weakly oriented:
                      activate(X) =  [10] X + [0]           
                                  >= [1] X + [0]            
                                  =  X                      
          
          activate(n__add(X1,X2)) =  [10] X1 + [10] X2 + [0]
                                  >= [10] X1 + [10] X2 + [4]
                                  =  add(X1,X2)             
          
             activate(n__from(X)) =  [0]                    
                                  >= [0]                    
                                  =  from(X)                
          
              activate(n__len(X)) =  [10] X + [0]           
                                  >= [10] X + [0]           
                                  =  len(X)                 
          
                          from(X) =  [0]                    
                                  >= [0]                    
                                  =  cons(X,n__from(s(X)))  
          
                          from(X) =  [0]                    
                                  >= [0]                    
                                  =  n__from(X)             
          
                       fst(X1,X2) =  [10] X1 + [10] X2 + [0]
                                  >= [1] X1 + [1] X2 + [1]  
                                  =  n__fst(X1,X2)          
          
                           len(X) =  [10] X + [0]           
                                  >= [1] X + [0]            
                                  =  n__len(X)              
          
                   len(cons(X,Z)) =  [10] Z + [0]           
                                  >= [10] Z + [1]           
                                  =  s(n__len(activate(Z))) 
          
                       len(nil()) =  [0]                    
                                  >= [1]                    
                                  =  0()                    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            activate(X) -> X
            activate(n__add(X1,X2)) -> add(X1,X2)
            activate(n__from(X)) -> from(X)
            activate(n__len(X)) -> len(X)
            from(X) -> cons(X,n__from(s(X)))
            from(X) -> n__from(X)
            fst(X1,X2) -> n__fst(X1,X2)
            len(X) -> n__len(X)
            len(cons(X,Z)) -> s(n__len(activate(Z)))
            len(nil()) -> 0()
        - Weak TRS:
            activate(n__fst(X1,X2)) -> fst(X1,X2)
            add(X1,X2) -> n__add(X1,X2)
            add(0(),X) -> X
            add(s(X),Y) -> s(n__add(activate(X),Y))
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
        - Signature:
            {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons
            ,n__add,n__from,n__fst,n__len,nil,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(n__add) = {1},
            uargs(n__fst) = {1,2},
            uargs(n__len) = {1},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [4]                  
            p(activate) = [1] x1 + [0]         
                 p(add) = [1] x1 + [1] x2 + [4]
                p(cons) = [1] x2 + [0]         
                p(from) = [0]                  
                 p(fst) = [1] x1 + [1] x2 + [7]
                 p(len) = [1] x1 + [3]         
              p(n__add) = [1] x1 + [1] x2 + [2]
             p(n__from) = [0]                  
              p(n__fst) = [1] x1 + [1] x2 + [7]
              p(n__len) = [1] x1 + [5]         
                 p(nil) = [0]                  
                   p(s) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
          activate(n__len(X)) = [1] X + [5]
                              > [1] X + [3]
                              = len(X)     
          
          
          Following rules are (at-least) weakly oriented:
                      activate(X) =  [1] X + [0]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
          activate(n__add(X1,X2)) =  [1] X1 + [1] X2 + [2]                  
                                  >= [1] X1 + [1] X2 + [4]                  
                                  =  add(X1,X2)                             
          
             activate(n__from(X)) =  [0]                                    
                                  >= [0]                                    
                                  =  from(X)                                
          
          activate(n__fst(X1,X2)) =  [1] X1 + [1] X2 + [7]                  
                                  >= [1] X1 + [1] X2 + [7]                  
                                  =  fst(X1,X2)                             
          
                       add(X1,X2) =  [1] X1 + [1] X2 + [4]                  
                                  >= [1] X1 + [1] X2 + [2]                  
                                  =  n__add(X1,X2)                          
          
                       add(0(),X) =  [1] X + [8]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
                      add(s(X),Y) =  [1] X + [1] Y + [4]                    
                                  >= [1] X + [1] Y + [2]                    
                                  =  s(n__add(activate(X),Y))               
          
                          from(X) =  [0]                                    
                                  >= [0]                                    
                                  =  cons(X,n__from(s(X)))                  
          
                          from(X) =  [0]                                    
                                  >= [0]                                    
                                  =  n__from(X)                             
          
                       fst(X1,X2) =  [1] X1 + [1] X2 + [7]                  
                                  >= [1] X1 + [1] X2 + [7]                  
                                  =  n__fst(X1,X2)                          
          
                       fst(0(),Z) =  [1] Z + [11]                           
                                  >= [0]                                    
                                  =  nil()                                  
          
              fst(s(X),cons(Y,Z)) =  [1] X + [1] Z + [7]                    
                                  >= [1] X + [1] Z + [7]                    
                                  =  cons(Y,n__fst(activate(X),activate(Z)))
          
                           len(X) =  [1] X + [3]                            
                                  >= [1] X + [5]                            
                                  =  n__len(X)                              
          
                   len(cons(X,Z)) =  [1] Z + [3]                            
                                  >= [1] Z + [5]                            
                                  =  s(n__len(activate(Z)))                 
          
                       len(nil()) =  [3]                                    
                                  >= [4]                                    
                                  =  0()                                    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            activate(X) -> X
            activate(n__add(X1,X2)) -> add(X1,X2)
            activate(n__from(X)) -> from(X)
            from(X) -> cons(X,n__from(s(X)))
            from(X) -> n__from(X)
            fst(X1,X2) -> n__fst(X1,X2)
            len(X) -> n__len(X)
            len(cons(X,Z)) -> s(n__len(activate(Z)))
            len(nil()) -> 0()
        - Weak TRS:
            activate(n__fst(X1,X2)) -> fst(X1,X2)
            activate(n__len(X)) -> len(X)
            add(X1,X2) -> n__add(X1,X2)
            add(0(),X) -> X
            add(s(X),Y) -> s(n__add(activate(X),Y))
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
        - Signature:
            {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons
            ,n__add,n__from,n__fst,n__len,nil,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(n__add) = {1},
            uargs(n__fst) = {1,2},
            uargs(n__len) = {1},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [2]                  
            p(activate) = [2] x1 + [2]         
                 p(add) = [2] x1 + [1] x2 + [1]
                p(cons) = [1] x1 + [1] x2 + [0]
                p(from) = [2] x1 + [0]         
                 p(fst) = [2] x1 + [2] x2 + [2]
                 p(len) = [2] x1 + [0]         
              p(n__add) = [1] x1 + [1] x2 + [0]
             p(n__from) = [1] x1 + [0]         
              p(n__fst) = [1] x1 + [1] x2 + [0]
              p(n__len) = [1] x1 + [0]         
                 p(nil) = [0]                  
                   p(s) = [1] x1 + [1]         
          
          Following rules are strictly oriented:
                      activate(X) = [2] X + [2]          
                                  > [1] X + [0]          
                                  = X                    
          
          activate(n__add(X1,X2)) = [2] X1 + [2] X2 + [2]
                                  > [2] X1 + [1] X2 + [1]
                                  = add(X1,X2)           
          
             activate(n__from(X)) = [2] X + [2]          
                                  > [2] X + [0]          
                                  = from(X)              
          
                       fst(X1,X2) = [2] X1 + [2] X2 + [2]
                                  > [1] X1 + [1] X2 + [0]
                                  = n__fst(X1,X2)        
          
          
          Following rules are (at-least) weakly oriented:
          activate(n__fst(X1,X2)) =  [2] X1 + [2] X2 + [2]                  
                                  >= [2] X1 + [2] X2 + [2]                  
                                  =  fst(X1,X2)                             
          
              activate(n__len(X)) =  [2] X + [2]                            
                                  >= [2] X + [0]                            
                                  =  len(X)                                 
          
                       add(X1,X2) =  [2] X1 + [1] X2 + [1]                  
                                  >= [1] X1 + [1] X2 + [0]                  
                                  =  n__add(X1,X2)                          
          
                       add(0(),X) =  [1] X + [5]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
                      add(s(X),Y) =  [2] X + [1] Y + [3]                    
                                  >= [2] X + [1] Y + [3]                    
                                  =  s(n__add(activate(X),Y))               
          
                          from(X) =  [2] X + [0]                            
                                  >= [2] X + [1]                            
                                  =  cons(X,n__from(s(X)))                  
          
                          from(X) =  [2] X + [0]                            
                                  >= [1] X + [0]                            
                                  =  n__from(X)                             
          
                       fst(0(),Z) =  [2] Z + [6]                            
                                  >= [0]                                    
                                  =  nil()                                  
          
              fst(s(X),cons(Y,Z)) =  [2] X + [2] Y + [2] Z + [4]            
                                  >= [2] X + [1] Y + [2] Z + [4]            
                                  =  cons(Y,n__fst(activate(X),activate(Z)))
          
                           len(X) =  [2] X + [0]                            
                                  >= [1] X + [0]                            
                                  =  n__len(X)                              
          
                   len(cons(X,Z)) =  [2] X + [2] Z + [0]                    
                                  >= [2] Z + [3]                            
                                  =  s(n__len(activate(Z)))                 
          
                       len(nil()) =  [0]                                    
                                  >= [2]                                    
                                  =  0()                                    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            from(X) -> cons(X,n__from(s(X)))
            from(X) -> n__from(X)
            len(X) -> n__len(X)
            len(cons(X,Z)) -> s(n__len(activate(Z)))
            len(nil()) -> 0()
        - Weak TRS:
            activate(X) -> X
            activate(n__add(X1,X2)) -> add(X1,X2)
            activate(n__from(X)) -> from(X)
            activate(n__fst(X1,X2)) -> fst(X1,X2)
            activate(n__len(X)) -> len(X)
            add(X1,X2) -> n__add(X1,X2)
            add(0(),X) -> X
            add(s(X),Y) -> s(n__add(activate(X),Y))
            fst(X1,X2) -> n__fst(X1,X2)
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
        - Signature:
            {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons
            ,n__add,n__from,n__fst,n__len,nil,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(n__add) = {1},
            uargs(n__fst) = {1,2},
            uargs(n__len) = {1},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [2]                  
            p(activate) = [2] x1 + [0]         
                 p(add) = [2] x1 + [1] x2 + [3]
                p(cons) = [1] x2 + [1]         
                p(from) = [7]                  
                 p(fst) = [2] x1 + [2] x2 + [0]
                 p(len) = [2] x1 + [0]         
              p(n__add) = [1] x1 + [1] x2 + [2]
             p(n__from) = [4]                  
              p(n__fst) = [1] x1 + [1] x2 + [0]
              p(n__len) = [1] x1 + [3]         
                 p(nil) = [4]                  
                   p(s) = [1] x1 + [2]         
          
          Following rules are strictly oriented:
             from(X) = [7]                  
                     > [5]                  
                     = cons(X,n__from(s(X)))
          
             from(X) = [7]                  
                     > [4]                  
                     = n__from(X)           
          
          len(nil()) = [8]                  
                     > [2]                  
                     = 0()                  
          
          
          Following rules are (at-least) weakly oriented:
                      activate(X) =  [2] X + [0]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
          activate(n__add(X1,X2)) =  [2] X1 + [2] X2 + [4]                  
                                  >= [2] X1 + [1] X2 + [3]                  
                                  =  add(X1,X2)                             
          
             activate(n__from(X)) =  [8]                                    
                                  >= [7]                                    
                                  =  from(X)                                
          
          activate(n__fst(X1,X2)) =  [2] X1 + [2] X2 + [0]                  
                                  >= [2] X1 + [2] X2 + [0]                  
                                  =  fst(X1,X2)                             
          
              activate(n__len(X)) =  [2] X + [6]                            
                                  >= [2] X + [0]                            
                                  =  len(X)                                 
          
                       add(X1,X2) =  [2] X1 + [1] X2 + [3]                  
                                  >= [1] X1 + [1] X2 + [2]                  
                                  =  n__add(X1,X2)                          
          
                       add(0(),X) =  [1] X + [7]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
                      add(s(X),Y) =  [2] X + [1] Y + [7]                    
                                  >= [2] X + [1] Y + [4]                    
                                  =  s(n__add(activate(X),Y))               
          
                       fst(X1,X2) =  [2] X1 + [2] X2 + [0]                  
                                  >= [1] X1 + [1] X2 + [0]                  
                                  =  n__fst(X1,X2)                          
          
                       fst(0(),Z) =  [2] Z + [4]                            
                                  >= [4]                                    
                                  =  nil()                                  
          
              fst(s(X),cons(Y,Z)) =  [2] X + [2] Z + [6]                    
                                  >= [2] X + [2] Z + [1]                    
                                  =  cons(Y,n__fst(activate(X),activate(Z)))
          
                           len(X) =  [2] X + [0]                            
                                  >= [1] X + [3]                            
                                  =  n__len(X)                              
          
                   len(cons(X,Z)) =  [2] Z + [2]                            
                                  >= [2] Z + [5]                            
                                  =  s(n__len(activate(Z)))                 
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            len(X) -> n__len(X)
            len(cons(X,Z)) -> s(n__len(activate(Z)))
        - Weak TRS:
            activate(X) -> X
            activate(n__add(X1,X2)) -> add(X1,X2)
            activate(n__from(X)) -> from(X)
            activate(n__fst(X1,X2)) -> fst(X1,X2)
            activate(n__len(X)) -> len(X)
            add(X1,X2) -> n__add(X1,X2)
            add(0(),X) -> X
            add(s(X),Y) -> s(n__add(activate(X),Y))
            from(X) -> cons(X,n__from(s(X)))
            from(X) -> n__from(X)
            fst(X1,X2) -> n__fst(X1,X2)
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
            len(nil()) -> 0()
        - Signature:
            {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons
            ,n__add,n__from,n__fst,n__len,nil,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(n__add) = {1},
            uargs(n__fst) = {1,2},
            uargs(n__len) = {1},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [6]                  
            p(activate) = [1] x1 + [1]         
                 p(add) = [1] x1 + [1] x2 + [1]
                p(cons) = [1] x2 + [0]         
                p(from) = [1]                  
                 p(fst) = [1] x1 + [1] x2 + [0]
                 p(len) = [1] x1 + [7]         
              p(n__add) = [1] x1 + [1] x2 + [0]
             p(n__from) = [1]                  
              p(n__fst) = [1] x1 + [1] x2 + [0]
              p(n__len) = [1] x1 + [6]         
                 p(nil) = [0]                  
                   p(s) = [1] x1 + [2]         
          
          Following rules are strictly oriented:
          len(X) = [1] X + [7]
                 > [1] X + [6]
                 = n__len(X)  
          
          
          Following rules are (at-least) weakly oriented:
                      activate(X) =  [1] X + [1]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
          activate(n__add(X1,X2)) =  [1] X1 + [1] X2 + [1]                  
                                  >= [1] X1 + [1] X2 + [1]                  
                                  =  add(X1,X2)                             
          
             activate(n__from(X)) =  [2]                                    
                                  >= [1]                                    
                                  =  from(X)                                
          
          activate(n__fst(X1,X2)) =  [1] X1 + [1] X2 + [1]                  
                                  >= [1] X1 + [1] X2 + [0]                  
                                  =  fst(X1,X2)                             
          
              activate(n__len(X)) =  [1] X + [7]                            
                                  >= [1] X + [7]                            
                                  =  len(X)                                 
          
                       add(X1,X2) =  [1] X1 + [1] X2 + [1]                  
                                  >= [1] X1 + [1] X2 + [0]                  
                                  =  n__add(X1,X2)                          
          
                       add(0(),X) =  [1] X + [7]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
                      add(s(X),Y) =  [1] X + [1] Y + [3]                    
                                  >= [1] X + [1] Y + [3]                    
                                  =  s(n__add(activate(X),Y))               
          
                          from(X) =  [1]                                    
                                  >= [1]                                    
                                  =  cons(X,n__from(s(X)))                  
          
                          from(X) =  [1]                                    
                                  >= [1]                                    
                                  =  n__from(X)                             
          
                       fst(X1,X2) =  [1] X1 + [1] X2 + [0]                  
                                  >= [1] X1 + [1] X2 + [0]                  
                                  =  n__fst(X1,X2)                          
          
                       fst(0(),Z) =  [1] Z + [6]                            
                                  >= [0]                                    
                                  =  nil()                                  
          
              fst(s(X),cons(Y,Z)) =  [1] X + [1] Z + [2]                    
                                  >= [1] X + [1] Z + [2]                    
                                  =  cons(Y,n__fst(activate(X),activate(Z)))
          
                   len(cons(X,Z)) =  [1] Z + [7]                            
                                  >= [1] Z + [9]                            
                                  =  s(n__len(activate(Z)))                 
          
                       len(nil()) =  [7]                                    
                                  >= [6]                                    
                                  =  0()                                    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            len(cons(X,Z)) -> s(n__len(activate(Z)))
        - Weak TRS:
            activate(X) -> X
            activate(n__add(X1,X2)) -> add(X1,X2)
            activate(n__from(X)) -> from(X)
            activate(n__fst(X1,X2)) -> fst(X1,X2)
            activate(n__len(X)) -> len(X)
            add(X1,X2) -> n__add(X1,X2)
            add(0(),X) -> X
            add(s(X),Y) -> s(n__add(activate(X),Y))
            from(X) -> cons(X,n__from(s(X)))
            from(X) -> n__from(X)
            fst(X1,X2) -> n__fst(X1,X2)
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
            len(X) -> n__len(X)
            len(nil()) -> 0()
        - Signature:
            {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons
            ,n__add,n__from,n__fst,n__len,nil,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(cons) = {2},
            uargs(n__add) = {1},
            uargs(n__fst) = {1,2},
            uargs(n__len) = {1},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                  
            p(activate) = [4] x1 + [0]         
                 p(add) = [4] x1 + [4] x2 + [0]
                p(cons) = [1] x2 + [0]         
                p(from) = [0]                  
                 p(fst) = [4] x1 + [4] x2 + [5]
                 p(len) = [4] x1 + [4]         
              p(n__add) = [1] x1 + [1] x2 + [0]
             p(n__from) = [0]                  
              p(n__fst) = [1] x1 + [1] x2 + [2]
              p(n__len) = [1] x1 + [1]         
                 p(nil) = [2]                  
                   p(s) = [1] x1 + [2]         
          
          Following rules are strictly oriented:
          len(cons(X,Z)) = [4] Z + [4]           
                         > [4] Z + [3]           
                         = s(n__len(activate(Z)))
          
          
          Following rules are (at-least) weakly oriented:
                      activate(X) =  [4] X + [0]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
          activate(n__add(X1,X2)) =  [4] X1 + [4] X2 + [0]                  
                                  >= [4] X1 + [4] X2 + [0]                  
                                  =  add(X1,X2)                             
          
             activate(n__from(X)) =  [0]                                    
                                  >= [0]                                    
                                  =  from(X)                                
          
          activate(n__fst(X1,X2)) =  [4] X1 + [4] X2 + [8]                  
                                  >= [4] X1 + [4] X2 + [5]                  
                                  =  fst(X1,X2)                             
          
              activate(n__len(X)) =  [4] X + [4]                            
                                  >= [4] X + [4]                            
                                  =  len(X)                                 
          
                       add(X1,X2) =  [4] X1 + [4] X2 + [0]                  
                                  >= [1] X1 + [1] X2 + [0]                  
                                  =  n__add(X1,X2)                          
          
                       add(0(),X) =  [4] X + [0]                            
                                  >= [1] X + [0]                            
                                  =  X                                      
          
                      add(s(X),Y) =  [4] X + [4] Y + [8]                    
                                  >= [4] X + [1] Y + [2]                    
                                  =  s(n__add(activate(X),Y))               
          
                          from(X) =  [0]                                    
                                  >= [0]                                    
                                  =  cons(X,n__from(s(X)))                  
          
                          from(X) =  [0]                                    
                                  >= [0]                                    
                                  =  n__from(X)                             
          
                       fst(X1,X2) =  [4] X1 + [4] X2 + [5]                  
                                  >= [1] X1 + [1] X2 + [2]                  
                                  =  n__fst(X1,X2)                          
          
                       fst(0(),Z) =  [4] Z + [5]                            
                                  >= [2]                                    
                                  =  nil()                                  
          
              fst(s(X),cons(Y,Z)) =  [4] X + [4] Z + [13]                   
                                  >= [4] X + [4] Z + [2]                    
                                  =  cons(Y,n__fst(activate(X),activate(Z)))
          
                           len(X) =  [4] X + [4]                            
                                  >= [1] X + [1]                            
                                  =  n__len(X)                              
          
                       len(nil()) =  [12]                                   
                                  >= [0]                                    
                                  =  0()                                    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            activate(X) -> X
            activate(n__add(X1,X2)) -> add(X1,X2)
            activate(n__from(X)) -> from(X)
            activate(n__fst(X1,X2)) -> fst(X1,X2)
            activate(n__len(X)) -> len(X)
            add(X1,X2) -> n__add(X1,X2)
            add(0(),X) -> X
            add(s(X),Y) -> s(n__add(activate(X),Y))
            from(X) -> cons(X,n__from(s(X)))
            from(X) -> n__from(X)
            fst(X1,X2) -> n__fst(X1,X2)
            fst(0(),Z) -> nil()
            fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
            len(X) -> n__len(X)
            len(cons(X,Z)) -> s(n__len(activate(Z)))
            len(nil()) -> 0()
        - Signature:
            {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons
            ,n__add,n__from,n__fst,n__len,nil,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))